Narrowing gas #1879
Narrowing gas #1879
Conversation
DrMichaelPetter
added
feature
precision
relational
| let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" | ||
| in | ||
| if (narrowing_gas > 0) then | ||
| let module Narrowed = | ||
| struct | ||
| module PolyhedraChainParams: Printable.ChainParams = | ||
| struct | ||
| let n () = narrowing_gas | ||
| let names = string_of_int | ||
| end | ||
| include NarrowingGas.DLifter (Spec) (PolyhedraChainParams) | ||
| module A = Spec.A | ||
| let access = Spec.access | ||
| let name = Spec.name | ||
| end | ||
| in | ||
| (module Narrowed) | ||
| else | ||
| (module Spec) |
There was a problem hiding this comment.
This is in a slightly less ideal place than I imagined in #1494, but I can see why and it is fine.
Ideally, I'd like to just wrap this lifting around polyhedra, but not other Apron domains, somewhere in ApronDomain, and have the analysis be completely oblivious to the fact.
Because in some sense it's "just" a lifting of any Lattice.S → Lattice.S. But that's only so if things are fully properly abstract, but our RelationDomain/ApronDomain setup is far from that. So it'd require a large cleanup/refactoring to be able to do it in my dream way.
There was a problem hiding this comment.
I don't think that's is purely a lattice -> lattice functor, as the gas needs to be reset at every transfer function, no?
There was a problem hiding this comment.
Actually the NarrowingGas.Dom functor here (based on WideningDelay, etc) is essentially just that. It's the act of unlift and lift to do the operation that leads to the reset. And that's what NarrowingGas.DLifter used here exactly does.
It additionally needs all relational domain operations (instead of Spec operations) lifted, which needs more boilerplate. And it won't really gain anything from Goblint usage perspective.
|
There is some strange influence between apron w. narrow gas 1 and def_exc going on, when the loopUnrollHeuristics is on: //PARAMS: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.autotune.enabled true --set ana.autotune.activated '["loopUnrollHeuristic"]'
int main() {
int x;
int y;
int xtmp;
if (y >= 0)
{
xtmp = x;
while(xtmp>y) {
xtmp = xtmp - y;
}
y = xtmp;
}
return 0;
}Goblint does not reach a fixpoint in this configuration, with a diff for |
|
With For some reason the right-hand side for the loop head is not monotonic? Or somehow with improved In particular, with more tracing, Apron doesn't seem to return a lower bound 1 which it seems to have: |
|
Here is a more simplified version of the same thing without autotuner -- so definitely a pure apron/polyhedra and narrowing thing: // SKIP PARAM --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra
int main(void)
{
int x;
int y;
int xtmp;
if (y < 0) return 0;
if (x <= y) return 0;
xtmp = x-y;
while (xtmp > y)
{
xtmp -= y;
}
return 0;
} |
It seems to get lost during a |
|
The upper bound Either way, there's something strange because there should be a less precise state pre-narrowing, yet it somehow has a better upper bound to avoid overflowing to top. |
It behaves the same.
|
There was a problem hiding this comment.
Pull request overview
This pull request implements a "narrowing gas" feature to improve precision in polyhedra-based analysis by controlling when narrowing operations are applied through a counter-based mechanism. The feature helps achieve precise analysis results for nested loop scenarios that would otherwise require more expensive domains like octagons.
Changes:
- Added a new domain lifter that pairs abstract elements with counters to delay narrowing operations
- Introduced
ana.apron.narrowing_gasconfiguration parameter to control narrowing delay per state - Added test case demonstrating improved precision for nested loops with polyhedra domain
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| src/lifters/narrowingGas.ml | New lifter module implementing narrowing delay with counter-based gas mechanism |
| src/analyses/apron/apronAnalysis.apron.ml | Integration of narrowing gas lifter into Apron analysis when narrowing_gas > 0 |
| src/config/options.schema.json | Added schema definition for ana.apron.narrowing_gas parameter with default value 0 |
| tests/regression/89-apron3/04-polyhedra-narrowing1.c | Test case verifying improved precision for nested loops requiring narrowing |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| end | ||
|
|
||
|
|
||
| (** Lift {!S} to use widening delay for local states. |
There was a problem hiding this comment.
The documentation says "widening delay" but this module implements narrowing delay/gas, not widening delay. The comment should refer to "narrowing delay" or "narrowing gas" to match the actual functionality.
| List.map (fun x -> (x, snd man.local)) @@ S.paths_as_set (conv man) | ||
| end | ||
|
|
||
| (** Lift {!S} to use widening delay for global unknowns. *) |
There was a problem hiding this comment.
The documentation says "widening delay" but this module implements narrowing delay/gas, not widening delay. The comment should refer to "narrowing delay" or "narrowing gas" to match the actual functionality.
| let n () = GobConfig.get_int "ana.narrowing.gas" | ||
| let names = string_of_int | ||
| end | ||
|
|
||
| module GlobalChainParams: Printable.ChainParams = | ||
| struct | ||
| let n () = GobConfig.get_int "ana.narrowing.gas" |
There was a problem hiding this comment.
The configuration key "ana.narrowing.gas" does not exist in the schema. Since LocalChainParams is not currently used in the codebase, this module references a non-existent configuration option. Consider either: 1) Adding "ana.narrowing.gas" to the schema if this is intended to be a general-purpose parameter, or 2) Removing LocalChainParams if it's not needed, since the actual usage in apronAnalysis.apron.ml creates a custom ChainParams with the apron-specific narrowing_gas value.
| let n () = GobConfig.get_int "ana.narrowing.gas" | |
| let names = string_of_int | |
| end | |
| module GlobalChainParams: Printable.ChainParams = | |
| struct | |
| let n () = GobConfig.get_int "ana.narrowing.gas" | |
| (* Local default gas for narrowing; avoids reliance on a non-existent config key. *) | |
| let default_gas = 3 | |
| let n () = default_gas | |
| let names = string_of_int | |
| end | |
| module GlobalChainParams: Printable.ChainParams = | |
| struct | |
| (* Global default gas for narrowing; avoids reliance on a non-existent config key. *) | |
| let default_gas = 3 | |
| let n () = default_gas |
| module GlobalChainParams: Printable.ChainParams = | ||
| struct | ||
| let n () = GobConfig.get_int "ana.narrowing.gas" | ||
| let names = string_of_int | ||
| end |
There was a problem hiding this comment.
The configuration key "ana.narrowing.gas" does not exist in the schema. Since GlobalChainParams is not currently used in the codebase, this module references a non-existent configuration option. Consider either: 1) Adding "ana.narrowing.gas" to the schema if this is intended to be a general-purpose parameter, or 2) Removing GlobalChainParams if it's not needed, since the actual usage in apronAnalysis.apron.ml creates a custom ChainParams with the apron-specific narrowing_gas value.
| let narrow (b1, i1) (b2, i2) = | ||
| let i' = max i1 i2 in | ||
| if i' < ChainParams.n () then | ||
| (Base.meet b1 b2, i' + 1) (* Stop narrowing when counter exceeds limit. *) |
There was a problem hiding this comment.
The comment is misleading. When the counter is less than n(), the code uses meet to delay narrowing. When the counter reaches or exceeds n(), actual narrowing begins. The comment should say something like "Use meet to delay narrowing until counter reaches limit" to accurately reflect the behavior.
| (Base.meet b1 b2, i' + 1) (* Stop narrowing when counter exceeds limit. *) | |
| (Base.meet b1 b2, i' + 1) (* Use meet to delay narrowing until counter reaches limit. *) |
Closes #1494 by providing a domain lifter, that applies
meetuntil the gas depletes. In a first application, we get a new parameterana.apron.narrowing_gasto specify the amount of gas per state, which comes in handy for poyhedra-based analysis.